[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
enrich
bin-min-heap,
index-array
with
procedures bin_min_heap_empty# : binheap ;
bin_min_heap_is_empty# binheap : bool ;
bin_min_heap_insert# keyindex : binheap × array nonfunctional ;
bin_min_heap_remove# nat : binheap × array nonfunctional ;
bin_min_heap_update# nat × key : binheap × array nonfunctional ;
bin_min_heap_get_min# binheap : nat nondeterministic;
bin_min_heap_extract_min# : binheap × array × nat nonfunctional nondeterministic;
bin_min_heap_bubble_up# nat : binheap × array nonfunctional ;
bin_min_heap_bubble_down# nat : binheap × array nonfunctional ;
bin_min_heap_resize# nat : binheap nonfunctional ;
bin_min_heap_next_2pot nat : nat nonfunctional ;
variables isempty : bool;
minsize : nat;
declarations empty : bin_min_heap_empty#(; bh){bh := bin-heap(mkkeyarray(1), 0)};
is-empty : bin_min_heap_is_empty#(bh; isempty){isempty := bh.size = 0};
insert
: bin_min_heap_insert#(ki; bh, ar)
{if ¬ ki.idx < # ar then abort; bin_min_heap_resize#(bh.size + 1; bh); bh.ar[bh.size] := ki; ar[ki.idx].idx := bh.size;
bh.size := bh.size + 1; bin_min_heap_bubble_up#(bh.size - 1; bh, ar)
}
;
remove
: bin_min_heap_remove#(n; bh, ar)
{if ¬ n < bh.size then abort; bh.size := bh.size - 1;
if bh.size ≠ 0 ∧ bh.size ≠ n
then {bh.ar[n] := bh.ar[bh.size]; ar[bh.ar[n].idx].idx := n;
if n ≠ 0 ∧ bh.ar[n].key < bh.ar[(n - 1) / 2].key
then bin_min_heap_bubble_up#(n; bh, ar)
else bin_min_heap_bubble_down#(n; bh, ar)}
}
;
update
: bin_min_heap_update#(n, key; bh, ar)
{if ¬ n < bh.size then abort;
let key0 = bh.ar[n].key
in {bh.ar[n].key := key; if key < key0 then bin_min_heap_bubble_up#(n; bh, ar) else bin_min_heap_bubble_down#(n; bh, ar)}
}
;
get-min : bin_min_heap_get_min#(bh; n){if bh.size = 0 then abort; n := bh.ar[0].idx};
next-2pot : bin_min_heap_next_2pot(minsize; n){while n < minsize do n := n * 2};
extract-min
: bin_min_heap_extract_min#(; bh, ar, n)
{bin_min_heap_get_min#(bh; n); bh.size := bh.size - 1;
if bh.size ≠ 0 then {bh.ar[0] := bh.ar[bh.size]; ar[bh.ar[0].idx].idx := 0; bin_min_heap_bubble_down#(0; bh, ar)}
}
;
bubble-up
: bin_min_heap_bubble_up#(n; bh, ar)
{let m = n
in while m ≠ 0 ∧ bh.ar[m].key < bh.ar[(m - 1) / 2].key
do let ki = bh.ar[m], ki0 = bh.ar[(m - 1) / 2]
in {bh.ar[m] := ki0; ar[ki0.idx].idx := m; m := (m - 1) / 2; bh.ar[m] := ki; ar[ki.idx].idx := m}
}
;
bubble-down
: bin_min_heap_bubble_down#(n; bh, ar)
{let m = n
in while 2 * m + 1 < bh.size
∧ (bh.ar[2 * m + 1].key < bh.ar[m].key ∨ 2 * m + 2 < bh.size ∧ bh.ar[2 * m + 2].key < bh.ar[m].key)
do let ki = bh.ar[m], ki0 = bh.ar[2 * m + 1]
in if 2 * m + 2 < bh.size ∧ bh.ar[2 * m + 2].key < ki0.key
then let ki1 = bh.ar[2 * m + 2]
in {bh.ar[m] := ki1; ar[ki1.idx].idx := m; bh.ar[2 * m + 2] := ki; ar[ki.idx].idx := 2 * m + 2; m := 2 * m + 2}
else {bh.ar[m] := ki0; ar[ki0.idx].idx := m; bh.ar[2 * m + 1] := ki; ar[ki.idx].idx := 2 * m + 1; m := 2 * m + 1}
}
;
resize
: bin_min_heap_resize#(minsize; bh)
{if minsize > bh.size
then let n = # bh.ar
in {bin_min_heap_next_2pot(minsize; n); let kar = mkkeyarray(n) in {kar := copy(bh.ar, 0, kar, 0, bh.size); bh.ar := kar}}
}
;
end enrich